Nuprl Lemma : comb_for_set_blt_wf
13,42
postcript
pdf
(
p
,
a
,
b
,
z
.
a
<
b
)
p
:PosetSig
|
p
|
|
p
|
(
True)
latex
Up
sets
1
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
T
Lemmas
poset
sig
wf
,
set
car
wf
,
true
wf
,
squash
wf
,
set
blt
wf
origin
p,a,b,z. a <
b) 
p:PosetSig
|p||p|(
True)
p,a,b,z. a < b) p:PosetSig|p||p|(True) T
x:A. B(x)T